CyberinfraV1, France, Analysis, bibRecord, 000004

Practical interruptible conversations: Distributed dynamic veriﬁcation with multiparty session types and Python

Identifieur interne : 000004 ( France/Analysis ); précédent : 000003; suivant : 000005

Practical interruptible conversations: Distributed dynamic veriﬁcation with multiparty session types and Python

Auteurs : Romain Demangeon [France] ; Kohei Honda ; Raymond Hu ; Rumyana Neykova ; Nobuko Yoshida

Source :

Formal Methods in System Design [ 0925-9856 ] ; 2015.

RBID : Hal:hal-01146168

Abstract

The rigorous and comprehensive verification of communication-based software is an important engineering challenge in distributed systems. Drawn from our industrial collaborations (Ocean Observatories Initative, http://www.oceanobservatories.org/, JBoss Savara Project, http://www.jboss.org/savara) on Scribble, a choreography description language based on multiparty session types, and its theoretical foundations (Honda et al., in POPL, pp 273–284, 2008), this article proposes a dynamic verification framework for structured interruptible conversation programming. We first present our extension of Scribble to support the specification of asynchronously interruptible conversations. We then implement a concise API for conversation programming with interrupts in Python that enables session types properties to be dynamically verified for distributed processes. Finally, we expose the underlying theory of our interrupt mechanism, studying its syntax and semantics, its integration in MPST theory and proving the correctness of our design. Our framework ensures the global safety of a system in the presence of asynchronous interrupts through independent runtime monitoring of each endpoint, checking the conformance of the local execution trace to the specified protocol. The usability of our framework for describing and verifying choreographic communications has been tested by integration into the large scientific cyberinfrastructure developed by the Ocean Observatories Initiative. Asynchronous interrupts have proven expressive enough to represent and verify their main classes of communication patterns, including asynchronous streaming and various timeout-based protocols, without introducing any implicit synchronisations. Benchmarks show conversation programming and monitoring can be realised with little overhead.

Url:

https://hal.archives-ouvertes.fr/hal-01146168

DOI: 10.1007/s10703-014-0218-8

Affiliations:

France

Links toward previous steps (curation, corpus...)

to stream Hal, to step Corpus: 000009
to stream Hal, to step Curation: 000009
to stream Hal, to step Checkpoint: 000001
to stream Main, to step Merge: 000054
to stream Main, to step Curation: 000054
to stream Main, to step Exploration: 000054
to stream France, to step Extraction: 000004

Links to Exploration step

Hal:hal-01146168

Le document en format XML

<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en">Practical interruptible conversations: Distributed dynamic veriﬁcation with multiparty session types and Python</title>
<author><name sortKey="Demangeon, Romain" sort="Demangeon, Romain" uniqKey="Demangeon R" first="Romain" last="Demangeon">Romain Demangeon</name>
<affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-391379" status="VALID"><orgName>Algorithmes, Programmes et Résolution </orgName>
<orgName type="acronym">APR</orgName>
<desc><address><country key="FR"></country>
</address>
</desc>
<listRelation><relation active="#struct-233" type="direct"></relation>
<relation active="#struct-93591" type="indirect"></relation>
<relation name="UMR7606" active="#struct-441569" type="indirect"></relation>
</listRelation>
<tutelles><tutelle active="#struct-233" type="direct"><org type="laboratory" xml:id="struct-233" status="VALID"><idno type="RNSR">199712651U</idno>
<orgName>Laboratoire d'Informatique de Paris 6</orgName>
<orgName type="acronym">LIP6</orgName>
<desc><address><addrLine>4 Place JUSSIEU 75252 PARIS CEDEX 05</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.lip6.fr/</ref>
</desc>
<listRelation><relation active="#struct-93591" type="direct"></relation>
<relation name="UMR7606" active="#struct-441569" type="direct"></relation>
</listRelation>
</org>
</tutelle>
<tutelle active="#struct-93591" type="indirect"><org type="institution" xml:id="struct-93591" status="VALID"><orgName>Université Pierre et Marie Curie - Paris 6</orgName>
<orgName type="acronym">UPMC</orgName>
<desc><address><addrLine>4 place Jussieu - 75005 Paris</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.upmc.fr/</ref>
</desc>
</org>
</tutelle>
<tutelle name="UMR7606" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno>
<idno type="IdRef">02636817X</idno>
<orgName>Centre National de la Recherche Scientifique</orgName>
<orgName type="acronym">CNRS</orgName>
<date type="start">1939-10-19</date>
<desc><address><country key="FR"></country>
</address>
<ref type="url">http://www.cnrs.fr/</ref>
</desc>
</org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>France</country>
</affiliation>
</author>
<author><name sortKey="Honda, Kohei" sort="Honda, Kohei" uniqKey="Honda K" first="Kohei" last="Honda">Kohei Honda</name>
</author>
<author><name sortKey="Hu, Raymond" sort="Hu, Raymond" uniqKey="Hu R" first="Raymond" last="Hu">Raymond Hu</name>
</author>
<author><name sortKey="Neykova, Rumyana" sort="Neykova, Rumyana" uniqKey="Neykova R" first="Rumyana" last="Neykova">Rumyana Neykova</name>
</author>
<author><name sortKey="Yoshida, Nobuko" sort="Yoshida, Nobuko" uniqKey="Yoshida N" first="Nobuko" last="Yoshida">Nobuko Yoshida</name>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">HAL</idno>
<idno type="RBID">Hal:hal-01146168</idno>
<idno type="halId">hal-01146168</idno>
<idno type="halUri">https://hal.archives-ouvertes.fr/hal-01146168</idno>
<idno type="url">https://hal.archives-ouvertes.fr/hal-01146168</idno>
<idno type="doi">10.1007/s10703-014-0218-8</idno>
<date when="2015">2015</date>
<idno type="wicri:Area/Hal/Corpus">000009</idno>
<idno type="wicri:Area/Hal/Curation">000009</idno>
<idno type="wicri:Area/Hal/Checkpoint">000001</idno>
<idno type="wicri:doubleKey">0925-9856:2015:Demangeon R:practical:interruptible:conversations</idno>
<idno type="wicri:Area/Main/Merge">000054</idno>
<idno type="wicri:Area/Main/Curation">000054</idno>
<idno type="wicri:Area/Main/Exploration">000054</idno>
<idno type="wicri:Area/France/Extraction">000004</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en">Practical interruptible conversations: Distributed dynamic veriﬁcation with multiparty session types and Python</title>
<author><name sortKey="Demangeon, Romain" sort="Demangeon, Romain" uniqKey="Demangeon R" first="Romain" last="Demangeon">Romain Demangeon</name>
<affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-391379" status="VALID"><orgName>Algorithmes, Programmes et Résolution </orgName>
<orgName type="acronym">APR</orgName>
<desc><address><country key="FR"></country>
</address>
</desc>
<listRelation><relation active="#struct-233" type="direct"></relation>
<relation active="#struct-93591" type="indirect"></relation>
<relation name="UMR7606" active="#struct-441569" type="indirect"></relation>
</listRelation>
<tutelles><tutelle active="#struct-233" type="direct"><org type="laboratory" xml:id="struct-233" status="VALID"><idno type="RNSR">199712651U</idno>
<orgName>Laboratoire d'Informatique de Paris 6</orgName>
<orgName type="acronym">LIP6</orgName>
<desc><address><addrLine>4 Place JUSSIEU 75252 PARIS CEDEX 05</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.lip6.fr/</ref>
</desc>
<listRelation><relation active="#struct-93591" type="direct"></relation>
<relation name="UMR7606" active="#struct-441569" type="direct"></relation>
</listRelation>
</org>
</tutelle>
<tutelle active="#struct-93591" type="indirect"><org type="institution" xml:id="struct-93591" status="VALID"><orgName>Université Pierre et Marie Curie - Paris 6</orgName>
<orgName type="acronym">UPMC</orgName>
<desc><address><addrLine>4 place Jussieu - 75005 Paris</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.upmc.fr/</ref>
</desc>
</org>
</tutelle>
<tutelle name="UMR7606" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno>
<idno type="IdRef">02636817X</idno>
<orgName>Centre National de la Recherche Scientifique</orgName>
<orgName type="acronym">CNRS</orgName>
<date type="start">1939-10-19</date>
<desc><address><country key="FR"></country>
</address>
<ref type="url">http://www.cnrs.fr/</ref>
</desc>
</org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>France</country>
</affiliation>
</author>
<author><name sortKey="Honda, Kohei" sort="Honda, Kohei" uniqKey="Honda K" first="Kohei" last="Honda">Kohei Honda</name>
</author>
<author><name sortKey="Hu, Raymond" sort="Hu, Raymond" uniqKey="Hu R" first="Raymond" last="Hu">Raymond Hu</name>
</author>
<author><name sortKey="Neykova, Rumyana" sort="Neykova, Rumyana" uniqKey="Neykova R" first="Rumyana" last="Neykova">Rumyana Neykova</name>
</author>
<author><name sortKey="Yoshida, Nobuko" sort="Yoshida, Nobuko" uniqKey="Yoshida N" first="Nobuko" last="Yoshida">Nobuko Yoshida</name>
</author>
</analytic>
<idno type="DOI">10.1007/s10703-014-0218-8</idno>
<series><title level="j">Formal Methods in System Design</title>
<idno type="ISSN">0925-9856</idno>
<imprint><date type="datePub">2015</date>
</imprint>
</series>
</biblStruct>
</sourceDesc>
</fileDesc>
<profileDesc><textClass></textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">The rigorous and comprehensive verification of communication-based software is an important engineering challenge in distributed systems. Drawn from our industrial collaborations (Ocean Observatories Initative, http://www.oceanobservatories.org/, JBoss Savara Project, http://www.jboss.org/savara) on Scribble, a choreography description language based on multiparty session types, and its theoretical foundations (Honda et al., in POPL, pp 273–284, 2008), this article proposes a dynamic verification framework for structured interruptible conversation programming. We first present our extension of Scribble to support the specification of asynchronously interruptible conversations. We then implement a concise API for conversation programming with interrupts in Python that enables session types properties to be dynamically verified for distributed processes. Finally, we expose the underlying theory of our interrupt mechanism, studying its syntax and semantics, its integration in MPST theory and proving the correctness of our design. Our framework ensures the global safety of a system in the presence of asynchronous interrupts through independent runtime monitoring of each endpoint, checking the conformance of the local execution trace to the specified protocol. The usability of our framework for describing and verifying choreographic communications has been tested by integration into the large scientific cyberinfrastructure developed by the Ocean Observatories Initiative. Asynchronous interrupts have proven expressive enough to represent and verify their main classes of communication patterns, including asynchronous streaming and various timeout-based protocols, without introducing any implicit synchronisations. Benchmarks show conversation programming and monitoring can be realised with little overhead.</div>
</front>
</TEI>
<affiliations><list><country><li>France</li>
</country>
</list>
<tree><noCountry><name sortKey="Honda, Kohei" sort="Honda, Kohei" uniqKey="Honda K" first="Kohei" last="Honda">Kohei Honda</name>
<name sortKey="Hu, Raymond" sort="Hu, Raymond" uniqKey="Hu R" first="Raymond" last="Hu">Raymond Hu</name>
<name sortKey="Neykova, Rumyana" sort="Neykova, Rumyana" uniqKey="Neykova R" first="Rumyana" last="Neykova">Rumyana Neykova</name>
<name sortKey="Yoshida, Nobuko" sort="Yoshida, Nobuko" uniqKey="Yoshida N" first="Nobuko" last="Yoshida">Nobuko Yoshida</name>
</noCountry>
<country name="France"><noRegion><name sortKey="Demangeon, Romain" sort="Demangeon, Romain" uniqKey="Demangeon R" first="Romain" last="Demangeon">Romain Demangeon</name>
</noRegion>
</country>
</tree>
</affiliations>
</record>

Pour manipuler ce document sous Unix (Dilib)

EXPLOR_STEP=$WICRI_ROOT/Ticri/CIDE/explor/CyberinfraV1/Data/France/Analysis

HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000004 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/France/Analysis/biblio.hfd -nk 000004 | SxmlIndent | more

Pour mettre un lien sur cette page dans le réseau Wicri

{{Explor lien
   |wiki=    Ticri/CIDE
   |area=    CyberinfraV1
   |flux=    France
   |étape=   Analysis
   |type=    RBID
   |clé=     Hal:hal-01146168
   |texte=   Practical interruptible conversations: Distributed dynamic veriﬁcation with multiparty session types and Python
}}

This area was generated with Dilib version V0.6.25.
Data generation: Thu Oct 27 09:30:58 2016. Site generation: Sun Mar 10 23:08:40 2024

	Serveur d'exploration Cyberinfrastructure
	Attention, ce site est en cours de développement ! Attention, site généré par des moyens informatiques à partir de corpus bruts. Les informations ne sont donc pas validées.

Serveur d'exploration Cyberinfrastructure

Practical interruptible conversations: Distributed dynamic veriﬁcation with multiparty session types and Python

Practical interruptible conversations: Distributed dynamic veriﬁcation with multiparty session types and Python

Source :

Abstract

Links toward previous steps (curation, corpus...)

Links to Exploration step

Le document en format XML

Pour manipuler ce document sous Unix (Dilib)

Pour mettre un lien sur cette page dans le réseau Wicri